ap(ap(map, f), xs) → ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) → null
ap(ap(ap(if, null), f), xs) → ap(ap(cons, ap(f, ap(last, xs))), ap(ap(if2, f), xs))
ap(ap(if2, f), xs) → ap(ap(map, f), ap(dropLast, xs))
ap(isEmpty, null) → true
ap(isEmpty, ap(ap(cons, x), xs)) → null
ap(last, ap(ap(cons, x), null)) → x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(last, ap(ap(cons, y), ys))
ap(dropLast, ap(ap(cons, x), null)) → null
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))
↳ QTRS
↳ DependencyPairsProof
ap(ap(map, f), xs) → ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) → null
ap(ap(ap(if, null), f), xs) → ap(ap(cons, ap(f, ap(last, xs))), ap(ap(if2, f), xs))
ap(ap(if2, f), xs) → ap(ap(map, f), ap(dropLast, xs))
ap(isEmpty, null) → true
ap(isEmpty, ap(ap(cons, x), xs)) → null
ap(last, ap(ap(cons, x), null)) → x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(last, ap(ap(cons, y), ys))
ap(dropLast, ap(ap(cons, x), null)) → null
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))
AP(ap(ap(if, null), f), xs) → AP(f, ap(last, xs))
AP(ap(ap(if, null), f), xs) → AP(ap(cons, ap(f, ap(last, xs))), ap(ap(if2, f), xs))
AP(ap(if2, f), xs) → AP(dropLast, xs)
AP(ap(ap(if, null), f), xs) → AP(ap(if2, f), xs)
AP(ap(if2, f), xs) → AP(map, f)
AP(ap(ap(if, null), f), xs) → AP(if2, f)
AP(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → AP(dropLast, ap(ap(cons, y), ys))
AP(ap(map, f), xs) → AP(ap(ap(if, ap(isEmpty, xs)), f), xs)
AP(ap(if2, f), xs) → AP(ap(map, f), ap(dropLast, xs))
AP(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → AP(last, ap(ap(cons, y), ys))
AP(ap(ap(if, null), f), xs) → AP(cons, ap(f, ap(last, xs)))
AP(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → AP(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))
AP(ap(map, f), xs) → AP(ap(if, ap(isEmpty, xs)), f)
AP(ap(map, f), xs) → AP(if, ap(isEmpty, xs))
AP(ap(map, f), xs) → AP(isEmpty, xs)
AP(ap(ap(if, null), f), xs) → AP(last, xs)
ap(ap(map, f), xs) → ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) → null
ap(ap(ap(if, null), f), xs) → ap(ap(cons, ap(f, ap(last, xs))), ap(ap(if2, f), xs))
ap(ap(if2, f), xs) → ap(ap(map, f), ap(dropLast, xs))
ap(isEmpty, null) → true
ap(isEmpty, ap(ap(cons, x), xs)) → null
ap(last, ap(ap(cons, x), null)) → x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(last, ap(ap(cons, y), ys))
ap(dropLast, ap(ap(cons, x), null)) → null
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
AP(ap(ap(if, null), f), xs) → AP(f, ap(last, xs))
AP(ap(ap(if, null), f), xs) → AP(ap(cons, ap(f, ap(last, xs))), ap(ap(if2, f), xs))
AP(ap(if2, f), xs) → AP(dropLast, xs)
AP(ap(ap(if, null), f), xs) → AP(ap(if2, f), xs)
AP(ap(if2, f), xs) → AP(map, f)
AP(ap(ap(if, null), f), xs) → AP(if2, f)
AP(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → AP(dropLast, ap(ap(cons, y), ys))
AP(ap(map, f), xs) → AP(ap(ap(if, ap(isEmpty, xs)), f), xs)
AP(ap(if2, f), xs) → AP(ap(map, f), ap(dropLast, xs))
AP(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → AP(last, ap(ap(cons, y), ys))
AP(ap(ap(if, null), f), xs) → AP(cons, ap(f, ap(last, xs)))
AP(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → AP(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))
AP(ap(map, f), xs) → AP(ap(if, ap(isEmpty, xs)), f)
AP(ap(map, f), xs) → AP(if, ap(isEmpty, xs))
AP(ap(map, f), xs) → AP(isEmpty, xs)
AP(ap(ap(if, null), f), xs) → AP(last, xs)
ap(ap(map, f), xs) → ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) → null
ap(ap(ap(if, null), f), xs) → ap(ap(cons, ap(f, ap(last, xs))), ap(ap(if2, f), xs))
ap(ap(if2, f), xs) → ap(ap(map, f), ap(dropLast, xs))
ap(isEmpty, null) → true
ap(isEmpty, ap(ap(cons, x), xs)) → null
ap(last, ap(ap(cons, x), null)) → x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(last, ap(ap(cons, y), ys))
ap(dropLast, ap(ap(cons, x), null)) → null
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
AP(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → AP(dropLast, ap(ap(cons, y), ys))
ap(ap(map, f), xs) → ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) → null
ap(ap(ap(if, null), f), xs) → ap(ap(cons, ap(f, ap(last, xs))), ap(ap(if2, f), xs))
ap(ap(if2, f), xs) → ap(ap(map, f), ap(dropLast, xs))
ap(isEmpty, null) → true
ap(isEmpty, ap(ap(cons, x), xs)) → null
ap(last, ap(ap(cons, x), null)) → x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(last, ap(ap(cons, y), ys))
ap(dropLast, ap(ap(cons, x), null)) → null
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
AP(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → AP(dropLast, ap(ap(cons, y), ys))
The value of delta used in the strict ordering is 256.
POL(ap(x1, x2)) = (2)x_1 + (4)x_2
POL(cons) = 4
POL(AP(x1, x2)) = (4)x_2
POL(dropLast) = 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
ap(ap(map, f), xs) → ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) → null
ap(ap(ap(if, null), f), xs) → ap(ap(cons, ap(f, ap(last, xs))), ap(ap(if2, f), xs))
ap(ap(if2, f), xs) → ap(ap(map, f), ap(dropLast, xs))
ap(isEmpty, null) → true
ap(isEmpty, ap(ap(cons, x), xs)) → null
ap(last, ap(ap(cons, x), null)) → x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(last, ap(ap(cons, y), ys))
ap(dropLast, ap(ap(cons, x), null)) → null
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
AP(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → AP(last, ap(ap(cons, y), ys))
ap(ap(map, f), xs) → ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) → null
ap(ap(ap(if, null), f), xs) → ap(ap(cons, ap(f, ap(last, xs))), ap(ap(if2, f), xs))
ap(ap(if2, f), xs) → ap(ap(map, f), ap(dropLast, xs))
ap(isEmpty, null) → true
ap(isEmpty, ap(ap(cons, x), xs)) → null
ap(last, ap(ap(cons, x), null)) → x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(last, ap(ap(cons, y), ys))
ap(dropLast, ap(ap(cons, x), null)) → null
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
AP(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → AP(last, ap(ap(cons, y), ys))
The value of delta used in the strict ordering is 256.
POL(ap(x1, x2)) = (2)x_1 + (4)x_2
POL(cons) = 4
POL(AP(x1, x2)) = (4)x_2
POL(last) = 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
ap(ap(map, f), xs) → ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) → null
ap(ap(ap(if, null), f), xs) → ap(ap(cons, ap(f, ap(last, xs))), ap(ap(if2, f), xs))
ap(ap(if2, f), xs) → ap(ap(map, f), ap(dropLast, xs))
ap(isEmpty, null) → true
ap(isEmpty, ap(ap(cons, x), xs)) → null
ap(last, ap(ap(cons, x), null)) → x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(last, ap(ap(cons, y), ys))
ap(dropLast, ap(ap(cons, x), null)) → null
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
AP(ap(ap(if, null), f), xs) → AP(f, ap(last, xs))
AP(ap(ap(if, null), f), xs) → AP(ap(if2, f), xs)
AP(ap(if2, f), xs) → AP(ap(map, f), ap(dropLast, xs))
AP(ap(map, f), xs) → AP(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(map, f), xs) → ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) → null
ap(ap(ap(if, null), f), xs) → ap(ap(cons, ap(f, ap(last, xs))), ap(ap(if2, f), xs))
ap(ap(if2, f), xs) → ap(ap(map, f), ap(dropLast, xs))
ap(isEmpty, null) → true
ap(isEmpty, ap(ap(cons, x), xs)) → null
ap(last, ap(ap(cons, x), null)) → x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(last, ap(ap(cons, y), ys))
ap(dropLast, ap(ap(cons, x), null)) → null
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
AP(ap(ap(if, null), f), xs) → AP(f, ap(last, xs))
Used ordering: Polynomial interpretation [25,35]:
AP(ap(ap(if, null), f), xs) → AP(ap(if2, f), xs)
AP(ap(if2, f), xs) → AP(ap(map, f), ap(dropLast, xs))
AP(ap(map, f), xs) → AP(ap(ap(if, ap(isEmpty, xs)), f), xs)
The value of delta used in the strict ordering is 1/2.
POL(null) = 0
POL(ap(x1, x2)) = 1/4 + (2)x_2
POL(cons) = 13/4
POL(AP(x1, x2)) = (2)x_1
POL(if) = 3
POL(last) = 3/2
POL(map) = 15/4
POL(true) = 15/4
POL(isEmpty) = 5/4
POL(if2) = 1/2
POL(dropLast) = 4
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
AP(ap(ap(if, null), f), xs) → AP(ap(if2, f), xs)
AP(ap(map, f), xs) → AP(ap(ap(if, ap(isEmpty, xs)), f), xs)
AP(ap(if2, f), xs) → AP(ap(map, f), ap(dropLast, xs))
ap(ap(map, f), xs) → ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) → null
ap(ap(ap(if, null), f), xs) → ap(ap(cons, ap(f, ap(last, xs))), ap(ap(if2, f), xs))
ap(ap(if2, f), xs) → ap(ap(map, f), ap(dropLast, xs))
ap(isEmpty, null) → true
ap(isEmpty, ap(ap(cons, x), xs)) → null
ap(last, ap(ap(cons, x), null)) → x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(last, ap(ap(cons, y), ys))
ap(dropLast, ap(ap(cons, x), null)) → null
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))